;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Ilist.lisp")

(module Mlist

  (defun firstn (n l)
    "The sublist of L consisting of its first N elements."
    (declare (xargs :guard (and (true-listp l)
                                (integerp n)
                                (<= 0 n))))
    (cond ((endp l) nil)
          ((zp n) nil)
          (t (cons (car l)
                   (firstn (1- n) (cdr l))))))
  
  (defun initial-sublistp (l1 l2)
    "Is the first list an initial sublist of the second?"
    (declare (xargs :guard (and (eqlable-listp l1)
                                (eqlable-listp l2))))
    (cond ((endp l1) t)
          ((endp l2) nil)
          (t (and (eql (car l1) (car l2))
                  (initial-sublistp (cdr l1) (cdr l2))))))

(defun initial-sublistp-eq (l1 l2)
  "Is the first list an initial sublist of the second?"
  (declare (xargs :guard (and (symbol-listp l1)
			      (symbol-listp l2))))
  (cond ((endp l1) t)
	((endp l2) nil)
	(t (and (eq (car l1) (car l2))
		(initial-sublistp-eq (cdr l1) (cdr l2))))))

(defun initial-sublistp-equal (l1 l2)
  "Is the first list an initial sublist of the second?"
  (declare (xargs :guard (and (true-listp l1)
			      (true-listp l2))))
  (cond ((endp l1) t)
	((endp l2) nil)
	(t (and (equal (car l1) (car l2))
		(initial-sublistp-equal (cdr l1) (cdr l2))))))

(defun memberp (x l)
  (DECLARE (XARGS :GUARD
		  (IF (EQLABLEP X)
		      (TRUE-LISTP L)
		      (EQLABLE-LISTP L))))
  (consp (member x l)))

(defun memberp-eq (x l)
  (declare (xargs :guard
		  (if (symbolp x)
		      (true-listp l)
		      (symbol-listp l))))
  (consp (member-eq x l)))

(defun memberp-equal (x l)
  (declare (xargs :guard (true-listp l)))
  (consp (member-equal x l)))

(defun no-duplicatesp-eq (l)
  (declare (xargs :guard (symbol-listp l)))
  (cond ((endp l) t)
	((member-eq (car l) (cdr l)) nil)
	(t (no-duplicatesp-equal (cdr l)))))

(defun nth-seg (i j l)
  "The sublist of L beginning at offset I for length J."
  (declare (xargs :guard (and (integerp i) (<= 0 i)
			      (integerp j) (<= 0 j)
			      (true-listp l))))
  (cond ((endp l) nil)
	((zp i)
	 (cond ((zp j) nil)
	       (t (cons (car l) (nth-seg i (1- j) (cdr l))))))
	(t (nth-seg (1- i) j (cdr l)))))

(defun occurrences-ac (item lst acc)
  (DECLARE (XARGS :GUARD
		  (AND (TRUE-LISTP LST)
		       (OR (EQLABLEP ITEM) (EQLABLE-LISTP LST))
		       (ACL2-NUMBERP ACC))))
  (cond ((endp lst) acc)
	((eql item (car lst)) (occurrences-ac item (cdr lst) (1+ acc)))
	(t (occurrences-ac item (cdr lst) acc))))
	 
(defun occurrences (item lst)
  (declare (xargs :guard (and (true-listp lst)
			      (or (eqlablep item) (eqlable-listp lst)))))
  (occurrences-ac item lst 0))

(defun occurrences-eq-ac (item lst acc)
  (DECLARE (XARGS :GUARD (and (true-listp lst)
			      (or (symbolp item)
				  (symbol-listp lst))
			      (ACL2-NUMBERP ACC))))
  (cond ((endp lst) acc)
	((eq item (car lst)) (occurrences-eq-ac item (cdr lst) (1+ acc)))
	(t (occurrences-eq-ac item (cdr lst) acc))))
	 
(defun occurrences-eq (item lst)
  (declare (xargs :guard (symbol-listp lst)))
  (occurrences-eq-ac item lst 0))

(defun occurrences-equal-ac (item lst acc)
  (DECLARE (XARGS :GUARD
		  (AND (TRUE-LISTP LST)
		       (ACL2-NUMBERP ACC))))
  (cond ((endp lst) acc)
	((equal item (car lst)) (occurrences-equal-ac item (cdr lst) (1+ acc)))
	(t (occurrences-equal-ac item (cdr lst) acc))))
	 
(defun occurrences-equal (item lst)
  (declare (xargs :guard (true-listp lst)))
  (occurrences-equal-ac item lst 0))

(defun put-nth (n v l)
  "The list derived from L by replacing its Nth element with value V."
  (declare (xargs :guard (and (integerp n) (<= 0 n)
			      (true-listp l))))
  (cond ((endp l) nil)
	((zp n) (cons v (cdr l)))
	(t (cons (car l) (put-nth (1- n) v (cdr l))))))

(defun put-seg (i seg l)
  "The list derived from L by replacing its contents beginning
   at location I with the contents of SEG. The length of the resulting
   list equals the length of L."
  (declare (xargs :guard (and (integerp i)
			      (<= 0 i)
			      (true-listp seg)
			      (true-listp l))))
  (cond ((endp l) nil)
	((zp i)
	 (cond ((endp seg) l)
	       (t (cons (car seg) (put-seg i (cdr seg) (cdr l))))))
	(t (cons (car l) (put-seg (1- i) seg (cdr l))))))

(defun remove-eq (x l)
  "The list constructed from L by removing all occurrences of X."
  (declare (xargs :guard (if (symbolp x)
			     (true-listp l)
			   (symbol-listp l))))
  (cond ((endp l) nil)
	((eq x (car l)) (remove-eq x (cdr l)))
	(t (cons (car l) (remove-eq x (cdr l))))))

(defun remove-equal (x l)
  "The list constructed from L by removing all occurrences of X."
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
	((equal x (car l)) (remove-equal x (cdr l)))
	(t (cons (car l) (remove-equal x (cdr l))))))

(defun remove-duplicates-eq (l)
  (declare (xargs :guard (symbol-listp l)))
  (cond ((endp l) nil)
	((member-eq (car l) (cdr l)) (remove-duplicates-eq (cdr l)))
	(t (cons (car l) (remove-duplicates-eq (cdr l))))))
  
  (defun sumlist (x)
  (if (consp x)
      (+ (car x)
         (sumlist (cdr x)))
    0))
  
  (export Ilist))

